\begin{tabbing}
$\forall$\=$A$, $B$:Type, $f$:($A$$\rightarrow$($B$ + Top)), ${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $X$:Interface(${\it ds}$;${\it da}$;$A$),\+
\\[0ex]${\it es}$:ES.
\-\\[0ex]es{-}decl(${\it es}$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$:\{$e$:E$\mid$ $\uparrow$($e$ $\in_{b}$ [[interface{-}compose($f$;$X$)]])\} .\+
\\[0ex][[interface{-}compose($f$;$X$)]]($e$) = do{-}apply($f$;[[$X$]]($e$)) $\in$ $B$)
\-
\end{tabbing}